$\forall$$a$:Id, $T$:Top, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:Top, ${\it init}$:$x$:Id fp$\rightarrow$ ${\it ds}$($x$)?Void, $x$:Id, $t$:Type, $v$:$t$.
\\[0ex]${\it ds}$ $\parallel$ $x$ : $t$
\\[0ex]$\Rightarrow$ ($x$ $\in$ dom(${\it init}$) $\Rightarrow$ ${\it init}$($x$) $=$ $v$)
\\[0ex]$\Rightarrow$ (with ds: ${\it ds}$ init: ${\it init}$action $a$:$T$ precondition $a$(v) is $P$ $\Vert\!+$ $x$ : $t$ initially $x$ = $v$)